; <lemma>
;  <title>ssf.7</title>
;  <origin>ssf | rec3 | cbuf_read/inv3/INV</origin>
(benchmark ssf_7
;  <theories>
;    <theory name="linear_order_int"/>
;    <theory name="basic_set"/>
;  </theories>
  :logic AUFLIA
;  <typenv>
;    <variable name="n" type="INTEGER"/>
;    <variable name="x" type="INTEGER"/>
;  </typenv>
  :extrafuns (
	       (n Int)
	       (x Int)
	       )
  :extramacros (
		 (in (lambda (?x 't) (?p ('t boolean)) . (?p ?x)))
		 (Nat (lambda (?i Int) . (<= 0 ?i)))
		 (range (lambda (?i1 Int) (?i2 Int) .
			  (lambda (?i Int) .
			    (and (<= ?i1 ?i) (<= ?i ?i2)))))
		 )
;  <hypothesis needed="true">not n = 0</hypothesis>
  :assumption (not (= n 0))
;  <hypothesis needed="true">x : 0 .. n</hypothesis>
  :assumption (in x (range 0 n))
;  <hypothesis needed="true">x &gt; 0</hypothesis>
  :assumption (> x 0)
;  <goal>x - 1 : 0 .. n</goal>
  :formula
  (not
    (in 
      (- x 1)
      (range 0 n))
    )
; </lemma>
)
